COMMENT ⊗   VALID 00004 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	NOTES ON AXIOMATIZING THE BLOCKS WORLD RELYING ON CIRCUMSCRIPTION
C00013 00003	LIST OF AXIOMS
C00016 00004	Remarks:
C00017 ENDMK
C⊗;
NOTES ON AXIOMATIZING THE BLOCKS WORLD RELYING ON CIRCUMSCRIPTION

			by John McCarthy

	We would like to describe moving by

∀ obj place. Move(obj,place) causes At(obj, place)

using

∀e p. e causes p  ⊃ ∀s.succeeds(e,s) ⊃ holds(p,result(e,s))

and using non-monotonic reasoning to determine when  Move(obj,place)
succeeds, what it changes and what remains unchanged.

	The frame problem is to be handled by

∀obj place. persistent At(obj,place)

and further non-monotonic reasoning.  In these notes we describe
what circumscriptions on what information will do the job, but we
don't yet have a fully coherent notion of how to express the common
sense knowledge in a way that insures that the right circumscriptions
will be done.


SUCCESS AND PREVENTION

∀obj place. Move(obj, place) causes At(obj, place)

∀e p. e causes p ⊃ ∀s. succeeds(e,s) ⊃ holds(p,result(e,s))

and consequently

∀obj place s. succeeds(Move(obj,place),s) 
			⊃ holds(At(obj,place),result(Move(obj,place),s)).


SUCCESS

∀obj place s. clear(top(obj),s) ∧ clear(place,s) ∧ ¬prevented(Move(obj,place),s)
		⊃ succeeds(Move(obj,place),s)

∀obj1 obj2 s. at(obj1,top(obj2),s) ⊃ unclear(obj2,s)

∀obj s. clear(obj,s) ≡ ¬unclear(obj,s)


FRAME

∀p e s. persistent p ∧ ¬changes(e,p) ∧ holds(p,s) ∧ successful(e,s)
				⊃ holds(p,result(e,s))

∀obj place place1. changes(Move(obj,place),At(obj,place1))

∀v e s.persistent1 v ∧ ¬changes1(e,v) ⊃ value(v,result(e,s)) = value(v,s)

∀obj place. persistent At(obj,place)

∀obj.persistent1 Color(obj)


PREVENTION

∀obj place s. tooheavy obj ⊃ prevented(Move(obj,place),s)

∀place place1 obj s. at(obj,place1,s) ∧ ¬close(place1,place,s)
				⊃ prevented(Move(obj,place),s)

Of course, there can be more axioms listing conditions that might
prevent moving.

∀place place1 place2 s.small(place) ∧ part(place1,place) ∧ part(place2,place)
				⊃ close(place1,place2,s)

∀obj place s.at(obj,place,s) ⊃ part(top(obj),place,s)

∀place1 place2 place3 s. part(place1,place2,s) ∧ part(place2,place3,s)
				⊃ part(place1,place3,s)


REIFICATIONS

∀obj place s. holds(At(obj,place),s) ≡ at(obj,place,s)

∀obj s.value(Color(obj),s) = color(obj,s)


THE PARTICULAR SITUATION S0

small(Table)

part(Place1,Table,S0)
part(Place2,Table,S0)
part(Place3,Table,S0)
part(Place4,Table,S0)

at(A,Place1,S0)
at(B,Place2,S0)
at(C,top(B),S0)
at(D,place5,S0)
at(E,place3,S0)

tooheavy A

color(A,S0) = Red
color(B,S0) = Red

color(C,S0) = Green ∨ color(E,S0) = Green

A ≠ B, etc.

disjoint(Place1,Place2), etc.

The last two should be obtained by some kind of non-monotonic reasoning,
but ordinary circumscription without the introduction of names won't work.
Reiter or somebody calls this "the unique names assumption".


USING CIRCUMSCRIPTION

	Suppose we want to put block  C  onto block  A  and then put
block  B  onto block  C.  The situation in question is

S2 = result(Move(B,top(C)),result(Move(C,top(A)),S0))

where  S0  is described above and is shown in the attached figure.
We want to show that

at(B,top(C),S2) ∧ at(C,top(A),S2)

in order to show success of our actions.  We may also want to show that
the other blocks are unmoved.

	We must first show

succeeds(Move(C,top(A),S0)

and this requires showing

clear(top(C),S0) ∧ clear(top(A),S0) ∧ ¬prevented(Move(C,top(A)),S0).

In the following reasoning, there will be some wishful thinking, but
we shall need ways of controlling the circumscription process so that
the wishful thinking turns into reality.

We infer  clear(top(C),S0)  by circumscribing   at(obj,place,S0)  or
perhaps just  at(obj,top(C),S0)  using all the availabile facts.
It isn't clear that this will go with all available facts because some
situation that is the result of actions might be  S0, and in that
situation  top(C)  might not be clear.  It isn't reasonable to presuppose
or even prove by circumscription that  S0  is a "Garden of Eden" situation,
because this information might not be available in other case where we
want to prove such facts.

	However, if we circumscribe using
just the known instances of  at(obj,top(C),S0), there aren't any.  Indeed
the only wffs whose conclusion includes  at(obj,place,s)  are the
result-of-moving rules.

clear(top(A),S0  is obtained similarly to  clear(top(C),S0).

In order to show that  ¬prevented(Move(C,top(A)),S0)  we circumscribe
prevented(Move(C,top(A),S0).  This requires showing
¬tooheavy(C)  which is also done by circumscription.
This at least is easy, since the only statement in which  tooheavy
occurs positively is  tooheavy(A),  but of course we are using the
fact that all the blocks are distinct.

The definition of  close  and the specific facts about  part  show
that  close(top(B),top(A)).  The condition  at(obj,place1,s)  in
the condition for non-closeness preventing moving specializes to
at(C,place1,S0),  and circumscribing   at(C,place1,S0)  shows that
this is the only place  C  is at.

Thus we have the premisses needed to establish

at(C,top(A),result(Move(C,top(A)),S0)).

Now we need to show that  B  and  C are clear and close in the
resulting situation and that  B  isn't too heavy.  The latter
property is not situation dependent, so it follows by the same
argument that previously established that  C  wasn't too heavy.

To establish closeness we need to use the persistence of  at
and to circumscribe  changes(Move(obj,place),At(obj,place1)).
This formalization may not be flexible enough for some purposes,
because  changes(e,p)  is not situtation dependent.


INDUCTION

	To prove that something cannot be done or to prove something
about all things that can be done, we need some induction axiom
schemes.  We introduce  canresult(s,s'),  meaning that the situation
s'  can be obtained from the situation  s  by some sequence of actions, by

∀s.canresult(s,s)

and

∀s s' a.canresult(s,s') ⊃ canresult(s,result(a,s')),

where the variable  a  is considered to range over those events which are
actions.

Circumscribing the predicate  canresult  in these two formulas leads
to the schema

∀s.(phi(s) ∧ ∀s' a.[phi(s') ⊃ phi(result(a,s'))] ⊃ ∀s'(phi(s') ⊃ canresult(s,s')).

Presumably it is best to take it as an axiom schema rather than conjecture
it by circumscription each time it is wanted.  Doing so amounts to assuming
that the only situations that can result from  s  are those that are
the consequences of a sequence of events.  This seems to embody what we
mean by "can result".

	A notion of achievable propositional fluents will be required.  We have

∀p s.∃s'.canresult(s,s') ∧ holds(p,s') ⊃ achievable(p,s),

but this is insufficient, because a fluent  p  may be achievable even though
no specific situation in which  p  holds is achievable, because  p  may
turn out to hold no matter which of two courses of events occurs.
LIST OF AXIOMS

Actions and events:

e1:	∀e p. e causes p ⊃ ∀s. succeeds(e,s) ⊃ holds(p,result(e,s))

e2:	∀p e s. persistent p ∧ ¬changes(e,p) ∧ holds(p,s) ∧ successful(e,s)
				⊃ holds(p,result(e,s))

e3:	∀v e s.persistent1 v ∧ ¬changes1(e,v) ⊃ value(v,result(e,s)) = value(v,s)


Moving objects:

m1:	∀obj place. Move(obj, place) causes At(obj, place)

m2:	∀obj place place1. changes(Move(obj,place),At(obj,place1))

m3:	∀obj place. persistent At(obj,place)

m4:	∀obj place s. clear(top(obj),s) ∧ clear(place,s) ∧ ¬prevented(Move(obj,place),s)
		⊃ succeeds(Move(obj,place),s)

m5:	∀obj1 obj2 s. at(obj1,top(obj2),s) ⊃ unclear(obj2,s)

m6:	∀obj s. clear(obj,s) ≡ ¬unclear(obj,s)

m7:	∀obj place s. tooheavy obj ⊃ prevented(Move(obj,place),s)

m8:	∀place place1 obj s. at(obj,place1,s) ∧ ¬close(place1,place,s)
				⊃ prevented(Move(obj,place),s)

m9:	∀place place1 place2 s.small(place) ∧ part(place1,place) ∧ part(place2,place)
				⊃ close(place1,place2,s)

m10:	∀obj place s.at(obj,place,s) ⊃ part(top(obj),place,s)

m11:	∀place1 place2 place3 s. part(place1,place2,s) ∧ part(place2,place3,s)
				⊃ part(place1,place3,s)



Coloring objects:

c1:	∀obj color. Paint(obj,color) causes Equal(color(obj),color)

This requires more reification than the formalization of  Move(obj,place)  and
suggest a different formalization.  Namely,

c1':	∀obj color. assigns(Paint(obj,color),color(obj), color)

together with the general axiom

e1':	∀e v val s.assigns(e,v,val) ∧ successful(e,s) ⊃ value(v,result(e,s)) = val

analogous to axiom  e1.

c2:	∀obj.persistent1 Color(obj)


REIFICATIONS

r1:	∀x y s.holds(Equal(x,y),s) ≡ value(x,s) = value(y,s)

r2:	∀obj place s. holds(At(obj,place),s) ≡ at(obj,place,s)

r3:	∀obj s.value(Color(obj),s) = color(obj,s)
Remarks:

1. Query: Can we conclude that all iterates of a function  f  are
distinct by some kind of non-monotonic reasoning, e.g. circumscription
of some higher order predicate?

	In particular, we wish to avoid having to show that nothing more
can be learned about the situation  S0  by reasoning from
it to future situations and then back to  S0.  This is true about
the blocks world but is often not true when purpose is involved.
For example, we may reason from the fact that a person wants  x
tomorrow that he will have done  y  yesterday to make it possible.